x:Id, k:Knd, ds:x:Id fp Type, da:a:Knd fp Type, f:(State(ds)Valtype(da;k)ds(x)?Void).
with declarations ds:dsda:daeffect of k(v) is x := f s v  MsgA 

latex

Definitions	MsgA, a:A fp B(a), with declarations ds:dsda:daeffect of k(v) is x := f s v, mk-ma, locl(a), , x : v, , IdDeq, <a, b>, State(ds), x:AB(x), Valtype(da;k), t.1, f(x)?z, KindDeq, rcv(l,tg), t.2, Type, Void, x:A  B(x), Id, , x:A. B(x), x. t(x), x.A(x), type List, IdLnk, t  T, Knd
Lemmas	Knd wf, IdLnk wf, fpf-empty wf, Id wf, pi2 wf, rcv wf, Kind-deq wf, fpf-cap wf, pi1 wf, ma-valtype wf, ma-state wf, id-deq wf, rationals wf, fpf-single wf, locl wf, mk-ma wf, fpf wf